1. Field of the Invention
Embodiments of the present invention generally relate to designing integrated circuits (ICs). More specifically, embodiments of the present invention relate to a method and a system for performing a compositional verification on an IC design that is both globally retimed and sequentially optimized.
2. Related Art
Dramatic improvements in semiconductor integration circuit (IC) technology presently make it possible to integrate hundreds of millions of transistors onto a single IC chip. These improvements in integration densities have been facilitated by advances in IC design and verification tools, which are now capable of designing and verifying ICs with ever-increasing complexity. In particular, one type of verification tool is used for performing equivalence checking to determine if two IC designs are functionally equivalent. As IC designs continue to become more complex, the task of verifying the equivalence between two IC designs becomes more complicated.
Among different equivalence checking tools, combinational equivalence checking (i.e., logic-level equivalence) has been the de facto standard technique for checking design equivalences for more than a decade. Meanwhile, many sequential optimization techniques have been developed that can make smaller and faster designs which consume less power. However, these sequential optimization techniques typically have to use sequential equivalence checking tools for design equivalence verification. Note that sequential equivalence checking can be a much harder verification problem than combinational equivalence checking, because the former typically requires sequential analysis on designs that often have a large number of registers. Note that the challenges associated with sequential equivalence checking become more pronounced for larger IC designs.
Recently, a number of practical techniques for performing sequential equivalence checking on fairly large designs have been proposed. In particular, one technique provides a compositional approach for performing sequential equivalence checking, which is referred to as “weak alignability” (see Z. Khasidashvili, et al., Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints, Proceedings of the International Conference on Computer-Aided Design, pp. 58-65, November 2004). Note that the term “alignability” was introduced by Pixley (C. Pixley, A theory and implementation of sequential hardware equivalence, IEEE Transactions on Computer-Aided Design, 11 (12):1469-1478, December 1992) as a notion of sequential equivalence without a known reset state. Weak alignability is a compositional extension of Pixley's original alignability which is not compositional. One important advantage of the weak alignability technique is that the compositionality is applicable to combinational equivalence checking and the verification can be performed on an abstraction/refinement scheme. However, a problem associated with the weak alignability technique is that the proposed compositionality cannot be efficiently applied to designs that are globally retimed (see I.-H. Moon, P. Bjesse, and C. Pixley, A compositional approach to the combination of combinational and sequential equivalence checking of circuits without known reset states, Proceedings of the Design Automation and Test in Europe Conference, pp. 1170-1175, 2007). This is because the equivalence on retimed design sub-blocks is broken even though the design equivalence is preserved.
Note that retiming is a sequential transformation technique that allows registers to be moved across combinational logic blocks while preserving the input/output behavior of the design. Moreover, although the registers can be moved across hierarchical boundaries during retiming, the design hierarchy is typically preserved. However, unlike other sequential optimization techniques (such as finite state machine (FSM) re-encoding/optimization, register merging/replication, etc.) which are local transformations, retiming is a global transformation that can be applied to a region of any size within a design. Consequently, it is generally difficult to verify retimed designs using conventional sequential verification techniques.
There are several proposed techniques for performing retiming verification. One such technique demonstrates that retiming can be verified by temporal equivalence which checks the number of registers on the corresponding cycles of two designs (see N. Shenoy, et al., On the temporal equivalence of sequential circuits, Proceedings of the Design Automation Conference, pp. 405-409, 1992, “Shenoy” hereafter). Another proposed technique verifies circuits which are both retimed and combinationally optimized by transforming a sequential equivalence problem into a combinational equivalence problem with the notion of a timed Boolean function that is represented with input values in multiple finite clock cycles (see R. K. Ranjan, et al., “Using combinational verification for sequential circuits,” in Proceedings of the Conference on Design Automation and Test in Europe, pages 9-12, 1999). Yet another proposed technique verifies retiming and combinational optimizations by recognizing retiming invariants as relationships between the registers of the two designs and checks the equivalence from the given initial states of the registers (see M. Mneimneh and K. Sakallah, Reverse: Efficient sequential verification for retiming, International Workshop on Logic Synthesis, 2003). However, all of these retiming verification techniques are restricted to designs that are either purely retimed without either sequential or combinational optimizations, or retimed with only combinational optimizations. Unfortunately, there is no known technique that can effectively verify designs that are both globally retimed and sequentially optimized through local transformations.
Hence, what is needed is a technique for performing sequential verifications on designs which are both globally retimed and sequentially optimized locally.